basic
Ident(T;op;id) == x:T. (x op id) = x & (id op x) = x 

latex

---

clarification:

basic
Ident(T;op;id) == x:T. (x op id) = x  T & (id op x) = x  T 

latex

Up	gen algebra 1
Wellformedness Lemmas	ident wf
Definitions	x:A. B(x), P & Q, x f y